M:MsgA, l:IdLnk, tg:Id. Dec(rcv(l,tg) declared in M) 

latex

Definitions	IdLnk, t  T, Id, Knd, x:A. B(x), x. t(x), a:A fp B(a), rcv(l,tg), KindDeq, x  dom(f), Dec(P), MsgA, rcv(l,tg) declared in M
Lemmas	msga wf, decidable assert, fpf-dom wf, Kind-deq wf, rcv wf, fpf-trivial-subtype-top, Knd wf, Id wf, IdLnk wf